ecase1($e$;${\it info}$;$i$.$f$($i$);$l$,${\it e'}$.$g$($l$;${\it e'}$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Case ${\it info}$($e$) of inl($p$) $\Rightarrow$ $f$(1of($p$)) ; inr($q$) $\Rightarrow$ $g$(1of(1of($q$));2of(1of($q$)))